Section: New Results

Reasoning over Distributed Systems

Participants : Vincent Armant, Philippe Chatalic, Philippe Dague, François Goasdoué, George Katsirelos, Laurent Simon, Lina Ye.

Distributed Diagnosis Problems

We pursued the work on distributed algorithms for diagnosing distributed systems. The general framework is consistency-based diagnosis for propositional-logic theories in a P2P setting with privacy constraints. It boils down to distributed implicant finding and is thus in some sense dual to the problem of consequence finding described in next paragraph. Vincent Armant is finishing is PhD and has extended his previous work on more general topics, i.e. focusing on the construction of a good decomposition of the network that will ensure an efficient reasoning mechanism. An important effort has been put in the design of a real-world sized experimentation on distributed systems.

Lina Ye defended her PhD on diagnosability analysis of distributed discrete-event systems, modeled as synchronized labeled automata. The aim of diagnosability is to ensure that a given partially observable system has the property that any fault (taken from a set of faults given a priori) will be detectable and identifiable without ambiguity in a finite time after its occurrence. Distributed diagnosability analysis is optimized by abstracting necessary and sufficient information from local objects to achieve global decision. After having addressed the distribution of the system's model into local models, we focus in 2011 on the extension to systems where the observable information itself is distributed instead of centralized. Joint diagnosability definition has been provided and undecidability of deciding it has been proved in the general case where communication events are not observable, before proposing an algorithm to test its sufficient condition. In addition, decidability result and algorithm have been given when communications are observable.

Michel Batteux defended also his PhD (led in the framework of a CIFRE thesis with Sherpa Engineering) about diagnosability and diagnosis of technological systems. The work was led in the centralized case, focusing on defining, implementing, testing and validating on a real case study (a fuel cell system) an all-in-one tool to design a diagnosis system for technological systems by integrating representation of the system and its potential faults, off-line diagnosability analysis and automatic generation of the on-line embedded diagnoser .

Distributed Consequence Finding

A major reengineering of the Somewhere platform, for decentralized consequence finding, has been initiated within the DisQuE project. Current efforts have focused on the rewriting of the communication layer, that now relies on the JXTA middleware. A new tool is also being developed, in order to facilitate large scale experimentations on a grid (Grid5000). This tool is designed in a fairly generic way, in order to be reusable for similar projects that require deploying sets of collaborating reasoners in a decentralized setting, and automating collaborative problem solving on various instances. We also expect this tool to be used for automating integration tests during further developments.

Towards distributed architectures for Modern SAT Solvers

If we aim at proposing a new architecture for distributed SAT Solvers, we pursued this year the improvements of Glucose, our centralized SAT solver. Glucose 2 won 3 medals at the SAT 2011 Competition, and one in the category Application SAT+UNSAT. We target to make a massively distributed version of Glucose, for very hard SAT problems.